e sends to i || a  == e'@i. (isrcv(e'))  (sender(e') = e)  val(e'):valtype(e')||a 

latex

---

clarification:

es-send-atom-to(es;e;a;i)
== alle-at(es;i;e'.(es-isrcv(es; e'))
==  (es-sender(es; e') = e  es-E(es))
==  free-from-atom{1}(es-valtype(es; e');es-val(es; e');a)) 

latex

Definitions	e@i. P(e), b, isrcv(e), P  Q, s = t, E, sender(e), x:T||a, valtype(e), val(e)
FDL editor aliases	es-send-atom-to